; COMMAND-LINE: --produce-difficulty
; EXPECT: sat
(set-logic QF_UFNRA)
(declare-fun m () Real)
(declare-fun set_prod (Real Real) Real)
(declare-fun --> (Real Real) Real)
(declare-fun mem (Real Real) Bool)
(declare-fun POW (Real) Real)
(declare-fun g_s0_1 () Real)
(declare-fun g_s1_0 () Real)
(declare-fun g_s2_2 () Real)
(declare-fun g_s3_3 () Real)
(declare-fun g_s4_4 () Real)
(declare-fun g_s5_5 () Real)
(declare-fun g_s6_6 () Real)
(declare-fun g_s7_7 () Real)
(declare-fun g_s8_8 () Real)
(declare-fun e10 () Real)
(declare-fun e12 () Real)
(declare-fun e9 () Real)
(declare-fun e11 () Real)
(declare-fun e16 () Real)
(declare-fun e15 () Real)
(declare-fun e14 () Real)
(declare-fun e13 () Real)
(assert (= g_s0_1 (/ (* m (- (/ e9 m) (/ 0 0.0))) 0.0)))
(assert (and (mem g_s0_1 (--> g_s1_0 (POW g_s1_0))) (mem g_s2_2 (--> g_s1_0 (POW g_s1_0))) (mem g_s3_3 (--> e11 (POW g_s1_0))) (mem g_s4_4 (--> g_s1_0 (POW g_s1_0))) (mem g_s5_5 (--> (set_prod g_s1_0 g_s1_0) (POW g_s1_0))) (mem g_s6_6 (--> (set_prod g_s1_0 g_s1_0) (POW g_s1_0))) (mem g_s7_7 (--> (set_prod g_s1_0 g_s1_0) (POW g_s1_0))) (mem g_s8_8 (--> (set_prod g_s1_0 g_s1_0) (POW g_s1_0))) (= g_s0_1 e9) (= g_s2_2 e10) (= g_s3_3 e11) (= g_s4_4 e12) (= g_s5_5 e13) (= g_s6_6 e14) (= g_s7_7 e15) (= g_s8_8 e16)))
(check-sat)
